T, T':Type{i}, L:(T List), f:({x:T| (x  L)} T'), P:(T'T'{i'}).
no_repeats(T;L)
 (x, y:T. (x  L)  (y  L)  ((x = y))  P(f(x),f(y)))
 (x,ymapl(f;L).  P(x,y)) 

latex

Definitions	Y, map(f;as), mapl(f;l), x:A. B(x), t  T, P  Q, ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), i  j < k, ||as||, {i..j}, l[i], P & Q, , A c B, x:A. B(x), {T}, P  Q, (x  l), P  Q, P  Q
Lemmas	l member wf, mapl wf, cons member, non neg length, length wf1, select member